Prop-NoImpredicativity.agda:4,8-26
Set₁ != Set
when checking that the expression {P : Prop} → P → P has type Prop
